(@$i$ $M$)($j$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$) then $M$ else  fi